$\forall$$T$:Type, $R$:($T$$\rightarrow$$T$$\rightarrow$prop\{i:l\}), $x$,$y$:$T$.
\\[0ex]($x$ rel\_star($T$; $R$) $y$) $\Leftarrow\!\Rightarrow$ (($\exists$$z$:$T$. (($x$ rel\_star($T$; $R$) $z$) $\wedge$ ($z$ $R$ $y$))) $\vee$ ($x$ = $y$))